i, x:Id, A:Realizer. x  dom(R-ds(A;i))  R-occurs(A;i;x) 

latex

Definitions

False, t  T, {T}, x:AB(x), Id, s = t, x:AB(x), P & Q, P  Q, Prop, x:A. B(x), a = b, b, Type, p  q, P  Q, P  Q, (x  l), IdDeq, deq-member(eq;x;L), P  Q, x.A(x), x. t(x), a:A fp B(a), Top, x  dom(f), left+right, p  q, , A, b, , Unit, source(l), Void, x:A. B(x), x : v, SQType(T), s ~ t, Atom$n, EqDecider(T), R-occurs(R;i;z), R-ds(R;i), f  g, es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, Knd, type List, IdLnk, State(ds), DeclaredType(ds;x), rec(x.A(x)), Realizer

Lemmas

es realizer wf, unit wf, decl-type wf, decl-state wf, IdLnk wf, Knd wf, fpf-join-dom, fpf-join wf, R-ds wf, fpf wf, R-occurs wf, fpf-single-dom, subtype rel self, deq wf, Id sq, fpf-single wf, lsrc wf, eqtt to assert, eqff to assert, assert of bnot, not functionality wrt iff, bool wf, bnot wf, not wf, fpf-empty wf, top wf, assert of bor, or functionality wrt iff, bor wf, fpf-dom wf, fpf-trivial-subtype-top, assert-deq-member, deq-member wf, l member wf, id-deq wf, implies functionality wrt iff, iff transitivity, assert of band, and functionality wrt iff, assert-eq-id, band wf, assert wf, eq id wf, Id wf, false wf